i:{...0}. |i| = (-i) 

latex

ProofTree

Definitions	True, ff, if b then t else f fi , , tt, t  T, x:A. B(x), {...i}
Lemmas	int lower wf, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf